1  /-
  2  Copyright (c) 2019 Kenny Lau, Chris Hughes. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Kenny Lau, Chris Hughes
  5  
  6  Direct limit of modules, abelian groups, rings, and fields.
  7  
  8  See Atiyah-Macdonald PP.32-33, Matsumura PP.269-270
  9  
 10  Generalizes the notion of "union", or "gluing", of incomparable modules over the same ring,
 11  or incomparable abelian groups, or rings, or fields.
 12  
 13  It is constructed as a quotient of the free module (for the module case) or quotient of
 14  the free commutative ring (for the ring case) instead of a quotient of the disjoint union
 15  so as to make the operations (addition etc.) "computable".
 16  -/
 17  
 18  import linear_algebra.direct_sum_module
src         └──────────────────────────────┘
 19  import algebra.big_operators
src         └───────────────────┘
 20  import ring_theory.free_comm_ring
src         └────────────────────────┘
 21  import ring_theory.ideal_operations
src         └──────────────────────────┘
 22  
 23  universes u v w u₁
 24  
 25  open lattice submodule
 26  
 27  variables {R : Type u} [ring R]
id                  └──┘     └──┘
src                          └──┘
typ                 └──┘     └──┘
 28  variables {ι : Type v} [nonempty ι]
id                  └──┘     └──────┘
src                          └──────┘
typ                 └──┘     └──────┘
 29  variables [directed_order ι] [decidable_eq ι]
id              └────────────┘     └──────────┘
src             └────────────┘     └──────────┘
typ             └────────────┘     └──────────┘
 30  variables (G : ι → Type w) [Π i, decidable_eq (G i)]
id                                  └──────────┘    
src                                   └──────────┘
typ                                 └──────────┘    
 31  
 32  /-- A directed system is a functor from the category (directed poset) to another category.
 33  This is used for abelian groups and rings and fields because their maps are not bundled.
 34  See module.directed_system -/
 35  class directed_system (f : Π i j, i ≤ j → G i → G j) : Prop :=
id                                             
src                                      
typ                                            
 36  (map_self : ∀ i x h, f i i h x = x)
id                           
src                                 
typ                          
 37  (map_map : ∀ i j k hij hjk x, f j k hjk (f i j hij x) = f i k (le_trans hij hjk) x)
id                   └─┘ └─┘      └─┘     └─┘        └──────┘ └─┘ └─┘  
src                                                               └──────┘
typ                  └─┘ └─┘      └─┘     └─┘        └──────┘ └─┘ └─┘  
 38  
 39  namespace module
 40  
 41  variables [Π i, add_comm_group (G i)] [Π i, module R (G i)]
id                  └────────────┘            └────┘      
src                  └────────────┘              └────┘
typ                 └────────────┘            └────┘      
doc                                              └────┘
 42  
 43  /-- A directed system is a functor from the category (directed poset) to the category of R-modules. -/
 44  class directed_system (f : Π i j, i ≤ j → G i →ₗ[R] G j) : Prop :=
id                                          └─┘  
src                                               └─┘ 
typ                                         └─┘  
 45  (map_self : ∀ i x h, f i i h x = x)
id                           
src                                 
typ                          
 46  (map_map : ∀ i j k hij hjk x, f j k hjk (f i j hij x) = f i k (le_trans hij hjk) x)
id                   └─┘ └─┘      └─┘     └─┘        └──────┘ └─┘ └─┘  
src                                                               └──────┘
typ                  └─┘ └─┘      └─┘     └─┘        └──────┘ └─┘ └─┘  
 47  
 48  variables (f : Π i j, i ≤ j → G i →ₗ[R] G j) [directed_system G f]
id                               └─┘       └─────────────┘
src                                   └─┘        └─────────────┘
typ                              └─┘       └─────────────┘
doc                                                └─────────────┘
 49  
 50  /-- The direct limit of a directed system is the modules glued together along the maps. -/
 51  def direct_limit : Type (max v w) :=
 52  (span R $ { a | ∃ (i j) (H : i ≤ j) x,
id    └──┘                      
src   └──┘                             
typ   └──┘                      
doc   └──┘
 53    direct_sum.lof R ι G i x - direct_sum.lof R ι G j (f i j H x) = a }).quotient
id     └────────────┘       └────────────┘                └──────┘
src    └────────────┘            └────────────┘                          └──────┘
typ    └────────────┘       └────────────┘                └──────┘
doc                                                                        └──────┘
 54  
 55  namespace direct_limit
 56  
 57  instance : add_comm_group (direct_limit G f) := quotient.add_comm_group _
id              └────────────┘  └──────────┘       └─────────────────────┘
src             └────────────┘  └──────────┘         └─────────────────────┘
typ             └────────────┘  └──────────┘       └─────────────────────┘
doc                             └──────────┘
 58  instance : module R (direct_limit G f) := quotient.module _
id              └────┘   └──────────┘       └─────────────┘
src             └────┘    └──────────┘         └─────────────┘
typ             └────┘   └──────────┘       └─────────────┘
doc             └────┘    └──────────┘
 59  
 60  variables (R ι)
 61  /-- The canonical map from a component to the direct limit. -/
 62  def of (i) : G i →ₗ[R] direct_limit G f :=
id                  └─┘ └──────────┘  
src                   └─┘  └──────────┘
typ                 └─┘ └──────────┘  
doc                         └──────────┘
 63  (mkq _).comp $ direct_sum.lof R ι G i
id    └─┘   └──┘    └────────────┘    
src   └─┘   └──┘    └────────────┘
typ   └─┘   └──┘    └────────────┘    
doc   └─┘
 64  variables {R ι G f}
 65  
 66  @[simp] lemma of_f {i j hij x} : (of R ι G f j (f i j hij x)) = of R ι G f i x :=
id                                     └┘          └─┘     └┘      
src                                    └┘                           └┘
typ                                    └┘          └─┘     └┘      
doc    └──┘                            └┘                            └┘
 67  eq.symm $ (submodule.quotient.eq _).2 $ subset_span ⟨i, j, hij, x, rfl⟩
id   └─────┘    └───────────────────┘       └─────────┘      └─┘    └─┘
src  └─────┘    └───────────────────┘       └─────────┘                └─┘
typ  └─────┘    └───────────────────┘       └─────────┘      └─┘    └─┘
 68  
 69  /-- Every element of the direct limit corresponds to some element in
 70  some component of the directed system. -/
 71  theorem exists_of (z : direct_limit G f) : ∃ i x, of R ι G f i x = z :=
id                          └──────────┘         └┘        
src                         └──────────┘             └┘             
typ                         └──────────┘         └┘        
doc                         └──────────┘               └┘
 72  nonempty.elim (by apply_instance) $ assume ind : ι,
id   └───────────┘                                    
src  └───────────┘     └────────────┘
typ  └───────────┘     └────────────┘                 
doc                    └────────────┘
txt                    └────────────┘
par                    └────────────┘
st                    └─────────────┘
 73  quotient.induction_on' z $ λ z, direct_sum.induction_on z
id   └────────────────────┘        └─────────────────────┘ 
src  └────────────────────┘          └─────────────────────┘
typ  └────────────────────┘        └─────────────────────┘ 
 74    ⟨ind, 0, linear_map.map_zero _⟩
id      └─┘     └─────────────────┘
src             └─────────────────┘
typ     └─┘     └─────────────────┘
 75    (λ i x, ⟨i, x, rfl⟩)
id                └─┘
src                   └─┘
typ               └─┘
 76    (λ p q ⟨i, x, ihx⟩ ⟨j, y, ihy⟩, let ⟨k, hik, hjk⟩ := directed_order.directed i j in
id                             └─┘    └─┘  └─┘     └─────────────────────┘
src                                                         └─────────────────────┘
typ                            └─┘    └─┘  └─┘     └─────────────────────┘
 77      ⟨k, f i k hik x + f j k hjk y, by rw [linear_map.map_add, of_f, of_f, ihx, ihy]; refl⟩)
id                                          └────────────────┘  └──┘  └──┘  └─┘  └─┘
src                                       └──┘└────────────────┘└┘└──┘└┘└──┘└┘   └┘     └──┘
typ                                     └──┘└────────────────┘└┘└──┘└┘└──┘└┘└─┘└┘└─┘  └──┘
doc                                        └──┘                  └┘    └┘    └┘   └┘     └──┘
txt                                        └──┘                  └┘    └┘    └┘   └┘     └──┘
par                                        └──┘                  └┘    └┘    └┘   └┘     └──┘
pid                                          └┘                  └┘    └┘    └┘   └┘   
st                                        └─────────────────────┘└────┘└─────────┘└───┘└────┘
 78  
 79  @[elab_as_eliminator]
doc    └────────────────┘
 80  protected theorem induction_on {C : direct_limit G f → Prop} (z : direct_limit G f)
id                                       └──────────┘                └──────────┘  
src                                      └──────────┘                  └──────────┘
typ                                      └──────────┘                └──────────┘  
doc                                      └──────────┘                  └──────────┘
 81    (ih : ∀ i x, C (of R ι G f i x)) : C z :=
id                  └┘            
src                    └┘
typ                 └┘            
doc                    └┘
 82  let ⟨i, x, h⟩ := exists_of z in h ▸ ih i x
id   └─┘           └───────┘        └┘
src                   └───────┘        
typ  └─┘           └───────┘        └┘
doc                   └───────┘
 83  
 84  variables {P : Type u₁} [add_comm_group P] [module R P] (g : Π i, G i →ₗ[R] P)
id                            └────────────┘     └────┘                  └─┘ 
src                           └────────────┘     └────┘                    └─┘ 
typ                           └────────────┘     └────┘                  └─┘ 
doc                                              └────┘
 85  variables (Hg : ∀ i j hij x, g j (f i j hij x) = g i x)
id                       └─┘           └─┘       
src                                                 
typ                      └─┘           └─┘       
 86  include Hg
 87  
 88  variables (R ι G f)
 89  /-- The universal property of the direct limit: maps from the components to another module
 90  that respect the directed system structure (i.e. make some diagram commute) give rise
 91  to a unique map out of the direct limit. -/
 92  def lift : direct_limit G f →ₗ[R] P :=
id              └──────────┘   └─┘ 
src             └──────────┘     └─┘ 
typ             └──────────┘   └─┘ 
doc             └──────────┘
 93  liftq _ (direct_sum.to_module R ι P g)
id   └───┘    └──────────────────┘    
src  └───┘    └──────────────────┘
typ  └───┘    └──────────────────┘    
doc  └───┘
 94    (span_le.2 $ λ a ⟨i, j, hij, x, hx⟩, by rw [← hx, mem_coe, linear_map.sub_mem_ker_iff,
id      └─────┘                                   └┘  └─────┘  └────────────────────────┘
src     └─────┘                               └────┘  └┘└─────┘└┘└────────────────────────┘└─
typ     └─────┘                             └────┘└┘└┘└─────┘└┘└────────────────────────┘└─
doc                                            └────┘  └┘       └┘                          └─
txt                                            └────┘  └┘       └┘                          └─
par                                            └────┘  └┘       └┘                          └─
pid                                              └──┘  └┘       └┘                          └─
st                                            └───────┘└───────┘└──────────────────────────┘└─
 95      direct_sum.to_module_lof, direct_sum.to_module_lof, Hg])
id       └──────────────────────┘  └──────────────────────┘  └┘
src  ───┘└──────────────────────┘└┘└──────────────────────┘└┘  
typ  ───┘└──────────────────────┘└┘└──────────────────────┘└┘└┘
doc  ───┘                        └┘                        └┘  
txt  ───┘                        └┘                        └┘  
par  ───┘                        └┘                        └┘  
pid  ───┘                        └┘                        └┘  
st   ───────────────────────────┘└────────────────────────┘└──┘
 96  variables {R ι G f}
 97  
 98  omit Hg
 99  lemma lift_of {i} (x) : lift R ι G f g Hg (of R ι G f i x) = g i x :=
id                           └──┘      └┘  └┘           
src                          └──┘               └┘              
typ                          └──┘      └┘  └┘           
doc                          └──┘               └┘
100  direct_sum.to_module_lof R _ _
id   └──────────────────────┘ 
src  └──────────────────────┘
typ  └──────────────────────┘ 
101  
102  theorem lift_unique (F : direct_limit G f →ₗ[R] P) (x) :
id                            └──────────┘   └─┘ 
src                           └──────────┘     └─┘ 
typ                           └──────────┘   └─┘ 
doc                           └──────────┘
103    F x = lift R ι G f (λ i, F.comp $ of R ι G f i)
id        └──┘          └───┘   └┘     
src         └──┘                └───┘   └┘
typ       └──┘          └───┘   └┘     
doc          └──┘                        └┘
104      (λ i j hij x, by rw [linear_map.comp_apply, of_f]; refl) x :=
id            └─┘          └───────────────────┘             
src                       └──┘└───────────────────┘└┘    └──┘
typ           └─┘      └──┘└───────────────────┘└┘    └──┘  
doc                       └──┘                     └┘      └──┘
txt                       └──┘                     └┘      └──┘
par                       └──┘                     └┘      └──┘
pid                         └┘                     └┘    
st                       └────────────────────────┘└─┘  └────┘
105  direct_limit.induction_on x $ λ i x, by rw lift_of; refl
id                                   
typ                                  
106  
107  section totalize
108  open_locale classical
109  variables (G f)
110  noncomputable def totalize : Π i j, G i →ₗ[R] G j :=
id                                       └─┘  
src                                          └─┘ 
typ                                      └─┘  
111  λ i j, if h : i ≤ j then f i j h else 0
id        └┘                      
src         └┘                            
typ       └┘                      
112  variables {G f}
113  
114  lemma totalize_apply (i j x) :
115    totalize G f i j x = if h : i ≤ j then f i j h x else 0 :=
id     └──────┘       └┘                       
src    └──────┘            └┘       
typ    └──────┘       └┘                       
116  if h : i ≤ j
id   └┘       
src  └┘       
typ  └┘       
117    then by dsimp only [totalize]; rw [dif_pos h, dif_pos h]
id                         └──────┘       └─────┘   └─────┘ 
src            └──────────┘└──────┘  └──┘└─────┘ └┘└─────┘ └─
typ            └──────────┘└──────┘  └──┘└─────┘└┘└─────┘└─
doc            └──────────┘          └──┘        └┘        └─
txt            └──────────┘          └──┘        └┘        └─
par            └──────────┘          └──┘        └┘        └─
pid                 └───┘└┘            └┘        └┘        
st            └──────────────────────────┘└───────┘└─────────┘
118    else by dsimp only [totalize]; rw [dif_neg h, dif_neg h, linear_map.zero_apply]
id                         └──────┘       └─────┘   └─────┘   └───────────────────┘
src  ─┘        └──────────┘└──────┘  └──┘└─────┘ └┘└─────┘ └┘└───────────────────┘└┘
typ  ─┘        └──────────┘└──────┘  └──┘└─────┘└┘└─────┘└┘└───────────────────┘└┘
doc  ─┘        └──────────┘          └──┘        └┘        └┘                     └┘
txt  ─┘        └──────────┘          └──┘        └┘        └┘                     └┘
par  ─┘        └──────────┘          └──┘        └┘        └┘                     └┘
pid  ─┘             └───┘└┘            └┘        └┘        └┘                     
st   ─┘       └──────────────────────────┘└───────┘└─────────┘└─────────────────────┘
119  end totalize
120  
121  lemma to_module_totalize_of_le {x : direct_sum ι G} {i j : ι}
id                                       └────────┘           
src                                      └────────┘
typ                                      └────────┘           
122    (hij : i ≤ j) (hx : ∀ k ∈ x.support, k ≤ i) :
id                           └──────┘    
src                             └──────┘    
typ                          └──────┘    
123    direct_sum.to_module R ι (G j) (λ k, totalize G f k j) x =
id     └──────────────────┘            └──────┘       
src    └──────────────────┘                 └──────┘            
typ    └──────────────────┘            └──────┘       
124    f i j hij (direct_sum.to_module R ι (G i) (λ k, totalize G f k i) x) :=
id        └─┘  └──────────────────┘            └──────┘      
src               └──────────────────┘                 └──────┘
typ       └─┘  └──────────────────┘            └──────┘      
125  begin
st   └─────
126    rw [← @dfinsupp.sum_single ι G _ _ _ x],
id            └─────────────────┘         
src    └────┘ └─────────────────┘  └─────┘ 
typ    └────┘ └─────────────────┘└─────┘
doc    └────┘                      └─────┘ 
txt    └────┘                      └─────┘ 
par    └────┘                      └─────┘ 
pid      └──┘                      └─────┘ 
st   ───────────────────────────────────────┘└──
127    unfold dfinsupp.sum,
src    └─────────────────┘
typ    └─────────────────┘
doc    └─────────────────┘
txt    └─────────────────┘
par    └─────────────────┘
pid          └───────────┘
st   ────────────────────┘
128    simp only [linear_map.map_sum],
129    refine finset.sum_congr rfl (λ k hk, _),
st                                            └─
130    rw direct_sum.single_eq_lof R k (x k),
id                                      
src    └─┘                             
typ    └─┘                          
doc    └─┘                             
txt    └─┘                             
par    └─┘                             
pid                                   
st   ────┘                        └────────┘
131    simp [totalize_apply, hx k hk, le_trans (hx k hk) hij, directed_system.map_map f]
id                                                
typ                                               
132  end
st   └─┘
133  
134  lemma of.zero_exact_aux {x : direct_sum ι G} (H : submodule.quotient.mk x = (0 : direct_limit G f)) :
id                                                                                               
typ                                                                                              
135    ∃ j, (∀ k ∈ x.support, k ≤ j) ∧ direct_sum.to_module R ι (G j) (λ i, totalize G f i j) x = (0 : G j) :=
id                                                                                             
typ                                                                                            
136  nonempty.elim (by apply_instance) $ assume ind : ι,
id                                                    
typ                                                   
137  span_induction ((quotient.mk_eq_zero _).1 H)
138    (λ x ⟨i, j, hij, y, hxy⟩, let ⟨k, hik, hjk⟩ := directed_order.directed i j in
id                                  
typ                                 
139      ⟨k, begin
140        clear_,
141        subst hxy,
142        split,
143        { intros i0 hi0,
144          rw [dfinsupp.mem_support_iff, dfinsupp.sub_apply, ← direct_sum.single_eq_lof,
145              ← direct_sum.single_eq_lof, dfinsupp.single_apply, dfinsupp.single_apply] at hi0,
146          split_ifs at hi0 with hi hj hj, { rwa hi at hik }, { rwa hi at hik }, { rwa hj at hjk },
st                                                           └┘                 └┘                 └┘
147          exfalso, apply hi0, rw sub_zero },
st                                           └┘
148        simp [linear_map.map_sub, totalize_apply, hik, hjk,
149          directed_system.map_map f, direct_sum.apply_eq_component,
150          direct_sum.component.of],
151      end⟩)
st       └─┘
152    ⟨ind, λ _ h, (finset.not_mem_empty _ h).elim, linear_map.map_zero _⟩
id      └─┘    
typ     └─┘    
153    (λ x y ⟨i, hi, hxi⟩ ⟨j, hj, hyj⟩,
id                         
typ                        
154      let ⟨k, hik, hjk⟩ := directed_order.directed i j in
id            
typ           
155      ⟨k, λ l hl,
id             
typ            
156        (finset.mem_union.1 (dfinsupp.support_add hl)).elim
157          (λ hl, le_trans (hi _ hl) hik)
158          (λ hl, le_trans (hj _ hl) hjk),
159        by simp [linear_map.map_add, hxi, hyj,
160            to_module_totalize_of_le hik hi,
161            to_module_totalize_of_le hjk hj]⟩)
162    (λ a x ⟨i, hi, hxi⟩,
id            
typ           
163      ⟨i, λ k hk, hi k (dfinsupp.support_smul hk),
id                     
typ                    
164        by simp [linear_map.map_smul, hxi]⟩)
165  
166  /-- A component that corresponds to zero in the direct limit is already zero in some
167  bigger module in the directed system. -/
168  theorem of.zero_exact {i x} (H : of R ι G f i x = 0) :
id                                             
typ                                            
169    ∃ j hij, f i j hij x = (0 : G j) :=
id                              
typ                             
170  let ⟨j, hj, hxj⟩ := of.zero_exact_aux H in
id        
typ       
171  if hx0 : x = 0 then ⟨i, le_refl _, by simp [hx0]⟩
id                       
typ                      
172  else
173    have hij : i ≤ j, from hj _ $
id                
typ               
174      by simp [direct_sum.apply_eq_component, hx0],
175    ⟨j, hij, by simpa [totalize_apply, hij] using hxj⟩
176  
177  end direct_limit
178  
179  end module
180  
181  
182  namespace add_comm_group
183  
184  variables [Π i, add_comm_group (G i)]
id                    └┘  └┘  └┘      
src                    └┘  └┘  └┘
typ                   └┘  └┘  └┘      
185  
186  /-- The direct limit of a directed system is the abelian groups glued together along the maps. -/
187  def direct_limit (f : Π i j, i ≤ j → G i → G j)
id                                        
src                                 
typ                                       
188    [Π i j hij, is_add_group_hom (f i j hij)] [directed_system G f] : Type* :=
id          └─┘  └──────────────┘     └─┘    └─────────────┘  
src                └──────────────┘               └─────────────┘
typ         └─┘  └──────────────┘     └─┘    └─────────────┘  
doc                └──────────────┘               └─────────────┘
189  @module.direct_limit ℤ _ ι _ _ _ G _ _ _
id    └─────────────────┘           
src   └─────────────────┘ 
typ   └─────────────────┘           
doc   └─────────────────┘
190    (λ i j hij, is_add_group_hom.to_linear_map $ f i j hij)
id          └─┘  └────────────────────────────┘      └─┘
src                └────────────────────────────┘
typ         └─┘  └────────────────────────────┘      └─┘
191    ⟨directed_system.map_self f, directed_system.map_map f⟩
id      └──────────────────────┘   └─────────────────────┘ 
src     └──────────────────────┘    └─────────────────────┘
typ     └──────────────────────┘   └─────────────────────┘ 
192  
193  namespace direct_limit
194  
195  variables (f : Π i j, i ≤ j → G i → G j)
id                                  
src                          
typ                                 
196  variables [Π i j hij, is_add_group_hom (f i j hij)] [directed_system G f]
id                  └─┘  └──────────────┘      └─┘    └─────────────┘
src                        └──────────────┘               └─────────────┘
typ                 └─┘  └──────────────┘      └─┘    └─────────────┘
doc                        └──────────────┘               └─────────────┘
197  
198  lemma directed_system : module.directed_system G (λ i j hij, is_add_group_hom.to_linear_map $ f i j hij) :=
id                           └────────────────────┘       └─┘  └────────────────────────────┘      └─┘
src                          └────────────────────┘               └────────────────────────────┘
typ                          └────────────────────┘       └─┘  └────────────────────────────┘      └─┘
doc                          └────────────────────┘
199  ⟨directed_system.map_self f, directed_system.map_map f⟩
id    └──────────────────────┘   └─────────────────────┘ 
src   └──────────────────────┘    └─────────────────────┘
typ   └──────────────────────┘   └─────────────────────┘ 
200  
201  local attribute [instance] directed_system
id                              └─────────────┘
src                             └─────────────┘
typ                             └─────────────┘
202  
203  instance : add_comm_group (direct_limit G f) :=
id              └────────────┘  └──────────┘  
src             └────────────┘  └──────────┘
typ             └────────────┘  └──────────┘  
doc                             └──────────┘
204  module.direct_limit.add_comm_group G (λ i j hij, is_add_group_hom.to_linear_map $ f i j hij)
id   └────────────────────────────────┘       └─┘  └────────────────────────────┘      └─┘
src  └────────────────────────────────┘               └────────────────────────────┘
typ  └────────────────────────────────┘       └─┘  └────────────────────────────┘      └─┘
205  
206  set_option class.instance_max_depth 50
doc             └──────────────────────┘
207  
208  /-- The canonical map from a component to the direct limit. -/
209  def of (i) : G i → direct_limit G f :=
id                    └──────────┘  
src                     └──────────┘
typ                   └──────────┘  
doc                     └──────────┘
210  module.direct_limit.of ℤ ι G (λ i j hij, is_add_group_hom.to_linear_map $ f i j hij) i
id                                                                                 
src                         
typ                                                                                
211  variables {G f}
212  
213  instance of.is_add_group_hom (i) : is_add_group_hom (of G f i) :=
id                                                              
typ                                                             
214  linear_map.is_add_group_hom _
215  
216  @[simp] lemma of_f {i j} (hij) (x) : of G f j (f i j hij x) = of G f i x :=
id                                                                   
typ                                                                  
doc    └──┘
217  module.direct_limit.of_f
218  
219  @[simp] lemma of_zero (i) : of G f i 0 = 0 := is_add_group_hom.map_zero _
id                                     
typ                                    
doc    └──┘
220  @[simp] lemma of_add (i x y) : of G f i (x + y) = of G f i x + of G f i y := is_add_hom.map_add _ _ _
id                                                                  
typ                                                                 
doc    └──┘
221  @[simp] lemma of_neg (i x) : of G f i (-x) = -of G f i x := is_add_group_hom.map_neg _ _
id                                                     
typ                                                    
doc    └──┘
222  @[simp] lemma of_sub (i x y) : of G f i (x - y) = of G f i x - of G f i y := is_add_group_hom.map_sub _ _ _
id                                                                  
typ                                                                 
doc    └──┘
223  
224  @[elab_as_eliminator]
doc    └────────────────┘
225  protected theorem induction_on {C : direct_limit G f → Prop} (z : direct_limit G f)
id                                                                                 
typ                                                                                
226    (ih : ∀ i x, C (of G f i x)) : C z :=
id                          
typ                         
227  module.direct_limit.induction_on z ih
228  
229  /-- A component that corresponds to zero in the direct limit is already zero in some
230  bigger module in the directed system. -/
231  theorem of.zero_exact (i x) (h : of G f i x = 0) : ∃ j hij, f i j hij x = 0 :=
id                                                                   
typ                                                                  
232  module.direct_limit.of.zero_exact h
233  
234  variables (P : Type u₁) [add_comm_group P]
id                            └────────────┘
src                           └────────────┘
typ                           └────────────┘
235  variables (g : Π i, G i → P) [Π i, is_add_group_hom (g i)]
id                                                      
typ                                                     
236  variables (Hg : ∀ i j hij x, g j (f i j hij x) = g i x)
id                                                
typ                                               
237  
238  variables (G f)
239  /-- The universal property of the direct limit: maps from the components to another abelian group
240  that respect the directed system structure (i.e. make some diagram commute) give rise
241  to a unique map out of the direct limit. -/
242  def lift : direct_limit G f → P :=
id                                
typ                               
243  module.direct_limit.lift ℤ ι G (λ i j hij, is_add_group_hom.to_linear_map $ f i j hij)
id                                                                             
src                           
typ                                                                            
244    (λ i, is_add_group_hom.to_linear_map $ g i) Hg
id                                             
typ                                            
245  variables {G f}
246  
247  instance lift.is_add_group_hom : is_add_group_hom (lift G f P g Hg) :=
id                                                              
typ                                                             
248  linear_map.is_add_group_hom _
249  
250  @[simp] lemma lift_of (i x) : lift G f P g Hg (of G f i x) = g i x :=
id                                                              
typ                                                             
doc    └──┘
251  module.direct_limit.lift_of _ _ _
252  
253  @[simp] lemma lift_zero : lift G f P g Hg 0 = 0 := is_add_group_hom.map_zero _
id                                     
typ                                    
doc    └──┘
254  @[simp] lemma lift_add (x y) : lift G f P g Hg (x + y) = lift G f P g Hg x + lift G f P g Hg y := is_add_hom.map_add _ _ _
id                                                                                    
typ                                                                                   
doc    └──┘
255  @[simp] lemma lift_neg (x) : lift G f P g Hg (-x) = -lift G f P g Hg x := is_add_group_hom.map_neg _ _
id                                                              
typ                                                             
doc    └──┘
256  @[simp] lemma lift_sub (x y) : lift G f P g Hg (x - y) = lift G f P g Hg x - lift G f P g Hg y := is_add_group_hom.map_sub _ _ _
id                                                                                    
typ                                                                                   
doc    └──┘
257  
258  lemma lift_unique (F : direct_limit G f → P) [is_add_group_hom F] (x) :
id                                            
typ                                           
259    F x = lift G f P (λ i x, F $ of G f i x) (λ i j hij x, by rw of_f) x :=
id                                                
typ                                               
260  direct_limit.induction_on x $ λ i x, by rw lift_of
id                                    
typ                                   
261  
262  end direct_limit
263  
264  end add_comm_group
265  
266  
267  namespace ring
268  
269  variables [Π i, comm_ring (G i)]
id                    └┘  └┘     
src                    └┘  └┘
typ                   └┘  └┘     
270  variables (f : Π i j, i ≤ j → G i → G j)
id                                  
src                          
typ                                 
271  variables [Π i j hij, is_ring_hom (f i j hij)]
id                  └─┘  └─────────┘      └─┘
src                        └─────────┘
typ                 └─┘  └─────────┘      └─┘
doc                        └─────────┘
272  variables [directed_system G f]
id              └─────────────┘
src             └─────────────┘
typ             └─────────────┘
doc             └─────────────┘
273  
274  open free_comm_ring
275  
276  /-- The direct limit of a directed system is the rings glued together along the maps. -/
277  def direct_limit : Type (max v w) :=
278  (ideal.span { a | (∃ i j H x, of (⟨j, f i j H x⟩ : Σ i, G i) - of ⟨i, x⟩ = a) ∨
id    └────────┘           └┘                   └┘         
src   └────────┘                └┘                            └┘            
typ   └────────┘           └┘                   └┘         
279    (∃ i, of (⟨i, 1⟩ : Σ i, G i) - 1 = a) ∨
id        └┘                     
src        └┘                          
typ       └┘                     
280    (∃ i x y, of (⟨i, x + y⟩ : Σ i, G i) - (of ⟨i, x⟩ + of ⟨i, y⟩) = a) ∨
id          └┘                  └┘       └┘          
src            └┘                        └┘         └┘             
typ         └┘                  └┘       └┘          
281    (∃ i x y, of (⟨i, x * y⟩ : Σ i, G i) - (of ⟨i, x⟩ * of ⟨i, y⟩) = a) }).quotient
id          └┘                  └┘       └┘            └──────┘
src            └┘                        └┘         └┘               └──────┘
typ         └┘                  └┘       └┘            └──────┘
282  
283  namespace direct_limit
284  
285  instance : comm_ring (direct_limit G f) :=
id              └───────┘  └──────────┘  
src             └───────┘  └──────────┘
typ             └───────┘  └──────────┘  
doc                        └──────────┘
286  ideal.quotient.comm_ring _
id   └──────────────────────┘
src  └──────────────────────┘
typ  └──────────────────────┘
287  
288  instance : ring (direct_limit G f) :=
id              └──┘  └──────────┘  
src             └──┘  └──────────┘
typ             └──┘  └──────────┘  
doc                   └──────────┘
289  comm_ring.to_ring _
id   └───────────────┘
src  └───────────────┘
typ  └───────────────┘
290  
291  /-- The canonical map from a component to the direct limit. -/
292  def of (i) (x : G i) : direct_limit G f :=
id                        └──────────┘  
src                         └──────────┘
typ                       └──────────┘  
doc                         └──────────┘
293  ideal.quotient.mk _ $ of ⟨i, x⟩
id   └───────────────┘     └┘    
src  └───────────────┘     └┘
typ  └───────────────┘     └┘    
294  
295  variables {G f}
296  
297  instance of.is_ring_hom (i) : is_ring_hom (of G f i) :=
id                                 └─────────┘  └┘   
src                                └─────────┘  └┘
typ                                └─────────┘  └┘   
doc                                └─────────┘  └┘
298  { map_one := ideal.quotient.eq.2 $ subset_span $ or.inr $ or.inl ⟨i, rfl⟩,
id                └───────────────┘    └─────────┘   └────┘   └────┘    └─┘
src               └───────────────┘    └─────────┘   └────┘   └────┘     └─┘
typ               └───────────────┘    └─────────┘   └────┘   └────┘    └─┘
299    map_mul := λ x y, ideal.quotient.eq.2 $ subset_span $ or.inr $ or.inr $ or.inr ⟨i, x, y, rfl⟩,
id                     └───────────────┘    └─────────┘   └────┘   └────┘   └────┘        └─┘
src                      └───────────────┘    └─────────┘   └────┘   └────┘   └────┘           └─┘
typ                    └───────────────┘    └─────────┘   └────┘   └────┘   └────┘        └─┘
300    map_add := λ x y, ideal.quotient.eq.2 $ subset_span $ or.inr $ or.inr $ or.inl ⟨i, x, y, rfl⟩ }
id                     └───────────────┘    └─────────┘   └────┘   └────┘   └────┘        └─┘
src                      └───────────────┘    └─────────┘   └────┘   └────┘   └────┘           └─┘
typ                    └───────────────┘    └─────────┘   └────┘   └────┘   └────┘        └─┘
301  
302  @[simp] lemma of_f {i j} (hij) (x) : of G f j (f i j hij x) = of G f i x :=
id                                        └┘        └─┘    └┘    
src                                       └┘                      └┘
typ                                       └┘        └─┘    └┘    
doc    └──┘                               └┘                       └┘
303  ideal.quotient.eq.2 $ subset_span $ or.inl ⟨i, j, hij, x, rfl⟩
id   └───────────────┘    └─────────┘   └────┘      └─┘    └─┘
src  └───────────────┘    └─────────┘   └────┘                └─┘
typ  └───────────────┘    └─────────┘   └────┘      └─┘    └─┘
304  
305  @[simp] lemma of_zero (i) : of G f i 0 = 0 := is_ring_hom.map_zero _
id                               └┘            └──────────────────┘
src                              └┘               └──────────────────┘
typ                              └┘            └──────────────────┘
doc    └──┘                      └┘                └──────────────────┘
306  @[simp] lemma of_one (i) : of G f i 1 = 1 := is_ring_hom.map_one _
id                              └┘            └─────────────────┘
src                             └┘               └─────────────────┘
typ                             └┘            └─────────────────┘
doc    └──┘                     └┘
307  @[simp] lemma of_add (i x y) : of G f i (x + y) = of G f i x + of G f i y := is_ring_hom.map_add _
id                                  └┘          └┘      └┘        └─────────────────┘
src                                 └┘               └┘          └┘            └─────────────────┘
typ                                 └┘          └┘      └┘        └─────────────────┘
doc    └──┘                         └┘                 └┘           └┘
308  @[simp] lemma of_neg (i x) : of G f i (-x) = -of G f i x := is_ring_hom.map_neg _
id                                └┘        └┘        └─────────────────┘
src                               └┘            └┘            └─────────────────┘
typ                               └┘        └┘        └─────────────────┘
doc    └──┘                       └┘               └┘            └─────────────────┘
309  @[simp] lemma of_sub (i x y) : of G f i (x - y) = of G f i x - of G f i y := is_ring_hom.map_sub _
id                                  └┘          └┘      └┘        └─────────────────┘
src                                 └┘               └┘          └┘            └─────────────────┘
typ                                 └┘          └┘      └┘        └─────────────────┘
doc    └──┘                         └┘                 └┘           └┘            └─────────────────┘
310  @[simp] lemma of_mul (i x y) : of G f i (x * y) = of G f i x * of G f i y := is_ring_hom.map_mul _
id                                  └┘          └┘      └┘        └─────────────────┘
src                                 └┘               └┘          └┘            └─────────────────┘
typ                                 └┘          └┘      └┘        └─────────────────┘
doc    └──┘                         └┘                 └┘           └┘
311  @[simp] lemma of_pow (i x) (n : ℕ) : of G f i (x ^ n) = of G f i x ^ n := is_semiring_hom.map_pow _ _ _
id                                       └┘          └┘          └─────────────────────┘
src                                      └┘               └┘               └─────────────────────┘
typ                                      └┘          └┘          └─────────────────────┘
doc    └──┘                               └┘                 └┘
312  
313  /-- Every element of the direct limit corresponds to some element in
314  some component of the directed system. -/
315  theorem exists_of (z : direct_limit G f) : ∃ i x, of G f i x = z :=
id                          └──────────┘         └┘      
src                         └──────────┘             └┘         
typ                         └──────────┘         └┘      
doc                         └──────────┘               └┘
316  nonempty.elim (by apply_instance) $ assume ind : ι,
id   └───────────┘                                    
src  └───────────┘     └────────────┘
typ  └───────────┘     └────────────┘                 
doc                    └────────────┘
txt                    └────────────┘
par                    └────────────┘
st                    └─────────────┘
317  quotient.induction_on' z $ λ x, free_abelian_group.induction_on x
id   └────────────────────┘        └─────────────────────────────┘ 
src  └────────────────────┘          └─────────────────────────────┘
typ  └────────────────────┘        └─────────────────────────────┘ 
318    ⟨ind, 0, of_zero ind⟩
id      └─┘     └─────┘ └─┘
src             └─────┘
typ     └─┘     └─────┘ └─┘
319    (λ s, multiset.induction_on s
id          └───────────────────┘ 
src          └───────────────────┘
typ         └───────────────────┘ 
320      ⟨ind, 1, of_one ind⟩
id        └─┘     └────┘ └─┘
src               └────┘
typ       └─┘     └────┘ └─┘
321      (λ a s ih, let ⟨i, x⟩ := a, ⟨j, y, hs⟩ := ih, ⟨k, hik, hjk⟩ := directed_order.directed i j in
id                                                
typ                                               
322        ⟨k, f i k hik x * f j k hjk y, by rw [of_mul, of_f, of_f, hs]; refl⟩))
id                                                                        └──┘
src                                                                       └──┘
typ                                                                       └──┘
doc                                                                       └──┘
323    (λ s ⟨i, x, ih⟩, ⟨i, -x, by rw [of_neg, ih]; refl⟩)
id                                                └──┘
src                                                 └──┘
typ                                               └──┘
doc                                                 └──┘
324    (λ p q ⟨i, x, ihx⟩ ⟨j, y, ihy⟩, let ⟨k, hik, hjk⟩ := directed_order.directed i j in
id                                      
typ                                     
325      ⟨k, f i k hik x + f j k hjk y, by rw [of_add, of_f, of_f, ihx, ihy]; refl⟩)
id                                                                            └──┘
src                                                                           └──┘
typ                                                                           └──┘
doc                                                                           └──┘
326  
327  @[elab_as_eliminator] theorem induction_on {C : direct_limit G f → Prop} (z : direct_limit G f)
id                                                                                             
typ                                                                                            
doc    └────────────────┘
328    (ih : ∀ i x, C (of G f i x)) : C z :=
id                          
typ                         
329  let ⟨i, x, hx⟩ := exists_of z in hx ▸ ih i x
id          
typ         
330  
331  section of_zero_exact
332  open_locale classical
333  variables (G f)
334  lemma of.zero_exact_aux2 {x : free_comm_ring Σ i, G i} {s t} (hxs : is_supported x s) {j k}
id                                 └────────────┘                   └──────────┘  
src                                └────────────┘                      └──────────┘
typ                                └────────────┘                   └──────────┘  
335    (hj : ∀ z : Σ i, G i, z ∈ s → z.1 ≤ j) (hk : ∀ z : Σ i, G i, z ∈ t → z.1 ≤ k)
id                                                         
src                                                                    
typ                                                        
336    (hjk : j ≤ k) (hst : s ⊆ t) :
id                         
src                          
typ                        
337    f j k hjk (lift (λ ix : s, f ix.1.1 j (hj ix ix.2) ix.1.2) (restriction s x)) =
id        └─┘  └──┘            └┘     └┘ └┘ └┘   └┘     └─────────┘     
src               └──┘                                        └─────────┘       
typ       └─┘  └──┘            └┘     └┘ └┘ └┘   └┘     └─────────┘     
338    lift (λ ix : t, f ix.1.1 k (hk ix ix.2) ix.1.2) (restriction t x) :=
id     └──┘            └┘     └┘ └┘ └┘   └┘     └─────────┘  
src    └──┘                                        └─────────┘
typ    └──┘            └┘     └┘ └┘ └┘   └┘     └─────────┘  
339  begin
340    refine ring.in_closure.rec_on hxs _ _ _ _,
341    { rw [restriction_one, lift_one, is_ring_hom.map_one (f j k hjk), restriction_one, lift_one] },
st                                                                                                  
342    { rw [restriction_neg, restriction_one, lift_neg, lift_one,
343        is_ring_hom.map_neg (f j k hjk), is_ring_hom.map_one (f j k hjk),
id                                                                   
typ                                                                  
344        restriction_neg, restriction_one, lift_neg, lift_one] },
st                                                              └┘
345    { rintros _ ⟨p, hps, rfl⟩ n ih,
346      rw [restriction_mul, lift_mul, is_ring_hom.map_mul (f j k hjk), ih, restriction_mul, lift_mul,
id                                                              
typ                                                             
347          restriction_of, dif_pos hps, lift_of, restriction_of, dif_pos (hst hps), lift_of],
348      dsimp only, rw directed_system.map_map f, refl },
st                                                      └┘
349    { rintros x y ihx ihy,
350      rw [restriction_add, lift_add, is_ring_hom.map_add (f j k hjk), ihx, ihy, restriction_add, lift_add] }
id                                                              
typ                                                             
st                                                                                                           └─
351  end
st   ──┘
352  variables {G f}
353  
354  lemma of.zero_exact_aux {x : free_comm_ring Σ i, G i} (H : ideal.quotient.mk _ x = (0 : direct_limit G f)) :
id                                                                                                      
typ                                                                                                     
355    ∃ j s, ∃ H : (∀ k : Σ i, G i, k ∈ s → k.1 ≤ j), is_supported x s ∧
id                                                                 
src                                                                     
typ                                                                
356      lift (λ ix : s, f ix.1.1 j (H ix ix.2) ix.1.2) (restriction s x) = (0 : G j) :=
id                                                                                
typ                                                                               
357  begin
358    refine span_induction (ideal.quotient.eq_zero_iff_mem.1 H) _ _ _ _,
359    { rintros x (⟨i, j, hij, x, rfl⟩ | ⟨i, rfl⟩ | ⟨i, x, y, rfl⟩ | ⟨i, x, y, rfl⟩),
360      { refine ⟨j, {⟨i, x⟩, ⟨j, f i j hij x⟩}, _,
id                                   
typ                                  
361          is_supported_sub (is_supported_of.2 $ or.inl rfl) (is_supported_of.2 $ or.inr $ or.inl rfl), _⟩,
362        { rintros k (rfl | ⟨rfl | h⟩), refl, exact hij, cases h },
st                                                                 └┘
363        { rw [restriction_sub, lift_sub, restriction_of, dif_pos, restriction_of, dif_pos, lift_of, lift_of],
364          dsimp only, rw directed_system.map_map f, exact sub_self _,
365          { left, refl }, { right, left, refl }, } },
st                        └┘                     └┘ └──┘
366      { refine ⟨i, {⟨i, 1⟩}, _, is_supported_sub (is_supported_of.2 $ or.inl rfl) is_supported_one, _⟩,
id                      
typ                     
367        { rintros k (rfl | h), refl, cases h },
st                                              └┘
368        { rw [restriction_sub, lift_sub, restriction_of, dif_pos, restriction_one, lift_of, lift_one],
369          dsimp only, rw [is_ring_hom.map_one (f i i _), sub_self], exact _inst_7 i i _, { left, refl } } },
id                                                                                    
typ                                                                                   
st                                                                                                       └────┘
370      { refine ⟨i, {⟨i, x+y⟩, ⟨i, x⟩, ⟨i, y⟩}, _,
id                         
typ                        
371          is_supported_sub (is_supported_of.2 $ or.inr $ or.inr $ or.inl rfl)
372            (is_supported_add (is_supported_of.2 $ or.inr $ or.inl rfl) (is_supported_of.2 $ or.inl rfl)), _⟩,
373        { rintros k (rfl | ⟨rfl | ⟨rfl | hk⟩⟩), refl, refl, refl, cases hk },
st                                                                            └┘
374        { rw [restriction_sub, restriction_add, restriction_of, restriction_of, restriction_of,
375            dif_pos, dif_pos, dif_pos, lift_sub, lift_add, lift_of, lift_of, lift_of],
376          dsimp only, rw is_ring_hom.map_add (f i i _), exact sub_self _,
id                                                   
typ                                                  
377          { right, right, left, refl }, { apply_instance }, { left, refl }, { right, left, refl } } },
st                                      └┘                  └┘              └┘                     └────┘
378      { refine ⟨i, {⟨i, x*y⟩, ⟨i, x⟩, ⟨i, y⟩}, _,
id                         
typ                        
379          is_supported_sub (is_supported_of.2 $ or.inr $ or.inr $ or.inl rfl)
380            (is_supported_mul (is_supported_of.2 $ or.inr $ or.inl rfl) (is_supported_of.2 $ or.inl rfl)), _⟩,
381        { rintros k (rfl | ⟨rfl | ⟨rfl | hk⟩⟩), refl, refl, refl, cases hk },
st                                                                            └┘
382        { rw [restriction_sub, restriction_mul, restriction_of, restriction_of, restriction_of,
383            dif_pos, dif_pos, dif_pos, lift_sub, lift_mul, lift_of, lift_of, lift_of],
384          dsimp only, rw is_ring_hom.map_mul (f i i _), exact sub_self _,
id                                                   
typ                                                  
385          { right, right, left, refl }, { apply_instance }, { left, refl }, { right, left, refl } } } },
st                                      └┘                  └┘              └┘                     └──────┘
386    { refine nonempty.elim (by apply_instance) (assume ind : ι, _),
id                                                              
typ                                                             
387      refine ⟨ind, ∅, λ _, false.elim, is_supported_zero, _⟩,
id               └─┘
typ              └─┘
388      rw [restriction_zero, lift_zero] },
st                                       └┘
389    { rintros x y ⟨i, s, hi, hxs, ihs⟩ ⟨j, t, hj, hyt, iht⟩,
390      rcases directed_order.directed i j with ⟨k, hik, hjk⟩,
id                                       
typ                                      
391      have : ∀ z : Σ i, G i, z ∈ s ∪ t → z.1 ≤ k,
id                                              
typ                                             
392      { rintros z (hz | hz), exact le_trans (hi z hz) hik, exact le_trans (hj z hz) hjk },
st                                                                                         └┘
393      refine ⟨k, s ∪ t, this, is_supported_add (is_supported_upwards hxs $ set.subset_union_left s t)
id               
typ              
394        (is_supported_upwards hyt $ set.subset_union_right s t), _⟩,
395      { rw [restriction_add, lift_add,
396          ← of.zero_exact_aux2 G f hxs hi this hik (set.subset_union_left s t),
id                                
typ                               
397          ← of.zero_exact_aux2 G f hyt hj this hjk (set.subset_union_right s t),
id                                
typ                               
398          ihs, is_ring_hom.map_zero (f i k hik), iht, is_ring_hom.map_zero (f j k hjk), zero_add] } },
id                                                                              
typ                                                                             
st                                                                                                  └──┘
399    { rintros x y ⟨j, t, hj, hyt, iht⟩, rw smul_eq_mul,
400      rcases exists_finset_support x with ⟨s, hxs⟩,
401      rcases (s.image sigma.fst).exists_le with ⟨i, hi⟩,
402      rcases directed_order.directed i j with ⟨k, hik, hjk⟩,
id                                       
typ                                      
403      have : ∀ z : Σ i, G i, z ∈ ↑s ∪ t → z.1 ≤ k,
id                                               
typ                                              
404      { rintros z (hz | hz), exact le_trans (hi z.1 $ finset.mem_image.2 ⟨z, hz, rfl⟩) hik, exact le_trans (hj z hz) hjk },
st                                                                                                                          └┘
405      refine ⟨k, ↑s ∪ t, this, is_supported_mul (is_supported_upwards hxs $ set.subset_union_left ↑s t)
id               
typ              
406        (is_supported_upwards hyt $ set.subset_union_right ↑s t), _⟩,
407      rw [restriction_mul, lift_mul,
408          ← of.zero_exact_aux2 G f hyt hj this hjk (set.subset_union_right ↑s t),
id                                
typ                               
409          iht, is_ring_hom.map_zero (f j k hjk), mul_zero] }
id                                         
typ                                        
st                                                           └─
410  end
st   ──┘
411  
412  /-- A component that corresponds to zero in the direct limit is already zero in some
413  bigger module in the directed system. -/
414  lemma of.zero_exact {i x} (hix : of G f i x = 0) : ∃ j, ∃ hij : i ≤ j, f i j hij x = 0 :=
id                                                                            
typ                                                                           
415  let ⟨j, s, H, hxs, hx⟩ := of.zero_exact_aux hix in
id        
typ       
416  have hixs : (⟨i, x⟩ : Σ i, G i) ∈ s, from is_supported_of.1 hxs,
id                             
typ                            
417  ⟨j, H ⟨i, x⟩ hixs, by rw [restriction_of, dif_pos hixs, lift_of] at hx; exact hx⟩
id            
typ           
418  end of_zero_exact
419  
420  /-- If the maps in the directed system are injective, then the canonical maps
421  from the components to the direct limits are injective. -/
422  theorem of_inj (hf : ∀ i j hij, function.injective (f i j hij)) (i) :
id                                                        
typ                                                       
423    function.injective (of G f i) :=
id                               
typ                              
424  begin
425    suffices : ∀ x, of G f i x = 0 → x = 0,
id                          
typ                         
426    { intros x y hxy, rw ← sub_eq_zero_iff_eq, apply this,
427      rw [is_ring_hom.map_sub (of G f i), hxy, sub_self] },
id                                      
typ                                     
st                                                         └┘
428    intros x hx, rcases of.zero_exact hx with ⟨j, hij, hfx⟩,
429    apply hf i j hij, rw [hfx, is_ring_hom.map_zero (f i j hij)]
id                                                       
typ                                                      
st                                                                
430  end
st   └─┘
431  
432  variables (P : Type u₁) [comm_ring P]
id                            └───────┘
src                           └───────┘
typ                           └───────┘
433  variables (g : Π i, G i → P) [Π i, is_ring_hom (g i)]
id                                                 
typ                                                
434  variables (Hg : ∀ i j hij x, g j (f i j hij x) = g i x)
id                                                 
typ                                                
435  include Hg
436  
437  open free_comm_ring
438  
439  variables (G f)
440  /-- The universal property of the direct limit: maps from the components to another ring
441  that respect the directed system structure (i.e. make some diagram commute) give rise
442  to a unique map out of the direct limit. -/
443  def lift : direct_limit G f → P :=
id                                
typ                               
444  ideal.quotient.lift _ (free_comm_ring.lift $ λ x, g x.1 x.2) begin
445    suffices : ideal.span _ ≤
446      ideal.comap (free_comm_ring.lift (λ (x : Σ (i : ι), G i), g (x.fst) (x.snd))) ⊥,
id                                                          
typ                                                         
447    { intros x hx, exact (mem_bot P).1 (this hx) },
id                                   
typ                                  
st                                                  └┘
448    rw ideal.span_le, intros x hx,
449    rw [mem_coe, ideal.mem_comap, mem_bot],
450    rcases hx with ⟨i, j, hij, x, rfl⟩ | ⟨i, rfl⟩ | ⟨i, x, y, rfl⟩ | ⟨i, x, y, rfl⟩;
451    simp only [lift_sub, lift_of, Hg, lift_one, lift_add, lift_mul,
452        is_ring_hom.map_one (g i), is_ring_hom.map_add (g i), is_ring_hom.map_mul (g i), sub_self]
id                                                                                    
typ                                                                                   
453  end
st   └─┘
454  variables {G f}
455  omit Hg
456  
457  instance lift.is_ring_hom : is_ring_hom (lift G f P g Hg) :=
id                                                    
typ                                                   
458  ⟨free_comm_ring.lift_one _,
459  λ x y, quotient.induction_on₂' x y $ λ p q, free_comm_ring.lift_mul _ _ _,
460  λ x y, quotient.induction_on₂' x y $ λ p q, free_comm_ring.lift_add _ _ _⟩
461  
462  @[simp] lemma lift_of (i x) : lift G f P g Hg (of G f i x) = g i x := free_comm_ring.lift_of _ _
id                                                              
typ                                                             
doc    └──┘
463  @[simp] lemma lift_zero : lift G f P g Hg 0 = 0 := is_ring_hom.map_zero _
id                                     
typ                                    
doc    └──┘
464  @[simp] lemma lift_one : lift G f P g Hg 1 = 1 := is_ring_hom.map_one _
id                                    
typ                                   
doc    └──┘
465  @[simp] lemma lift_add (x y) : lift G f P g Hg (x + y) = lift G f P g Hg x + lift G f P g Hg y := is_ring_hom.map_add _
id                                                                                    
typ                                                                                   
doc    └──┘
466  @[simp] lemma lift_neg (x) : lift G f P g Hg (-x) = -lift G f P g Hg x := is_ring_hom.map_neg _
id                                                              
typ                                                             
doc    └──┘
467  @[simp] lemma lift_sub (x y) : lift G f P g Hg (x - y) = lift G f P g Hg x - lift G f P g Hg y := is_ring_hom.map_sub _
id                                                                                    
typ                                                                                   
doc    └──┘
468  @[simp] lemma lift_mul (x y) : lift G f P g Hg (x * y) = lift G f P g Hg x * lift G f P g Hg y := is_ring_hom.map_mul _
id                                                                                    
typ                                                                                   
doc    └──┘
469  @[simp] lemma lift_pow (x) (n : ℕ) : lift G f P g Hg (x ^ n) = lift G f P g Hg x ^ n := is_semiring_hom.map_pow _ _ _
id                                                                                
src                                  
typ                                                                               
doc    └──┘
470  
471  theorem lift_unique (F : direct_limit G f → P) [is_ring_hom F] (x) :
id                                              
typ                                             
472    F x = lift G f P (λ i x, F $ of G f i x) (λ i j hij x, by rw [of_f]) x :=
id                                                
typ                                               
st                                                                       
473  direct_limit.induction_on x $ λ i x, by rw lift_of
id                                    
typ                                   
474  
475  end direct_limit
476  
477  end ring
478  
479  
480  namespace field
481  
482  variables [Π i, field (G i)]
id                    └┘     
src                    └┘
typ                   └┘     
483  variables (f : Π i j, i ≤ j → G i → G j) [Π i j hij, is_ring_hom (f i j hij)]
id                                         └─┘  └─────────┘      └─┘
src                                                      └─────────┘
typ                                        └─┘  └─────────┘      └─┘
doc                                                       └─────────┘
484  variables [directed_system G f]
id              └─────────────┘
src             └─────────────┘
typ             └─────────────┘
doc             └─────────────┘
485  
486  namespace direct_limit
487  
488  instance nonzero_comm_ring : nonzero_comm_ring (ring.direct_limit G f) :=
id                                └───────────────┘  └───────────────┘  
src                               └───────────────┘  └───────────────┘
typ                               └───────────────┘  └───────────────┘  
doc                               └───────────────┘  └───────────────┘
489  { zero_ne_one := nonempty.elim (by apply_instance) $ assume i : ι, begin
id                    └───────────┘                                  
src                   └───────────┘     └────────────┘
typ                   └───────────┘     └────────────┘               
doc                                     └────────────┘
txt                                     └────────────┘
par                                     └────────────┘
st                                     └─────────────┘
490      change (0 : ring.direct_limit G f) ≠ 1,
491      rw ← ring.direct_limit.of_one,
492      intros H, rcases ring.direct_limit.of.zero_exact H.symm with ⟨j, hij, hf⟩,
id                                                            
src                                                           
typ                                                           
493      rw is_ring_hom.map_one (f i j hij) at hf,
id                                  └─┘
typ                                 └─┘
494      exact one_ne_zero hf
id             └─────────┘ └┘
src            └─────────┘
typ            └─────────┘ └┘
495    end,
st     └─┘
496    .. ring.direct_limit.comm_ring G f }
id        └─────────────────────────┘  
src       └─────────────────────────┘
typ       └─────────────────────────┘  
497  
498  theorem exists_inv {p : ring.direct_limit G f} : p ≠ 0 → ∃ y, p * y = 1 :=
id                           └───────────────┘                 
src                          └───────────────┘                       
typ                          └───────────────┘                 
doc                          └───────────────┘
499  ring.direct_limit.induction_on p $ λ i x H,
id   └────────────────────────────┘        
src  └────────────────────────────┘
typ  └────────────────────────────┘        
500  ⟨ring.direct_limit.of G f i (x⁻¹), by erw [← ring.direct_limit.of_mul,
id    └──────────────────┘     └┘
src   └──────────────────┘         └┘
typ   └──────────────────┘     └┘
doc   └──────────────────┘
501      mul_inv_cancel (assume h : x = 0, H $ by rw [h, ring.direct_limit.of_zero]),
st                                                                                
502      ring.direct_limit.of_one]⟩
st                               
503  
504  section
505  open_locale classical
506  
507  noncomputable def inv (p : ring.direct_limit G f) : ring.direct_limit G f :=
id                              └───────────────┘      └───────────────┘  
src                             └───────────────┘        └───────────────┘
typ                             └───────────────┘      └───────────────┘  
doc                             └───────────────┘        └───────────────┘
508  if H : p = 0 then 0 else classical.some (direct_limit.exists_inv G f H)
id   └┘                     └────────────┘                            
src  └┘                      └────────────┘
typ  └┘                     └────────────┘                            
509  
510  protected theorem mul_inv_cancel {p : ring.direct_limit G f} (hp : p ≠ 0) : p * inv G f p = 1 :=
id                                         └───────────────┘                   └─┘    
src                                        └───────────────┘                       └─┘       
typ                                        └───────────────┘                   └─┘    
doc                                        └───────────────┘
511  by rw [inv, dif_neg hp, classical.some_spec (direct_limit.exists_inv G f hp)]
512  
513  protected theorem inv_mul_cancel {p : ring.direct_limit G f} (hp : p ≠ 0) : inv G f p * p = 1 :=
id                                         └───────────────┘                 └─┘      
src                                        └───────────────┘                    └─┘          
typ                                        └───────────────┘                 └─┘      
doc                                        └───────────────┘
514  by rw [_root_.mul_comm, direct_limit.mul_inv_cancel G f hp]
515  
516  protected noncomputable def field : field (ring.direct_limit G f) :=
id                                       └───┘  └───────────────┘  
src                                      └───┘  └───────────────┘
typ                                      └───┘  └───────────────┘  
doc                                             └───────────────┘
517  { inv := inv G f,
id            └─┘  
src           └─┘
typ           └─┘  
518    mul_inv_cancel := λ p, direct_limit.mul_inv_cancel G f,
id                                                        
typ                                                       
519    inv_mul_cancel := λ p, direct_limit.inv_mul_cancel G f,
id                                                        
typ                                                       
520    .. direct_limit.nonzero_comm_ring G f }
id        └────────────────────────────┘  
src       └────────────────────────────┘
typ       └────────────────────────────┘  
521  
522  protected noncomputable def discrete_field : discrete_field (ring.direct_limit G f) :=
id                                                └────────────┘  └───────────────┘  
src                                               └────────────┘  └───────────────┘
typ                                               └────────────┘  └───────────────┘  
doc                                                               └───────────────┘
523  { has_decidable_eq := classical.dec_eq _,
id                         └──────────────┘
src                        └──────────────┘
typ                        └──────────────┘
524    inv_zero := dif_pos rfl,
id                 └─────┘ └─┘
src                └─────┘ └─┘
typ                └─────┘ └─┘
525    ..direct_limit.field G f }
id       └────────────────┘  
src      └────────────────┘
typ      └────────────────┘  
526  
527  end
528  
529  end direct_limit
530  
531  end field